n:. WellFnd{i}({...n};x,y.x > y) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), x,y. t(x;y), , P  Q, P & Q, P  Q, P  Q, True, T, i > j, x(s1,s2), {...i},
Lemmas	nat well founded, int lower wf, nat wf, inv image ind, add mono wrt lt, minus mono wrt lt, iff transitivity, wellfounded functionality wrt iff, true wf, squash wf, wellfounded wf